Crate isotope[−][src]
Expand description
The Isotope Project
isotope
is an experimental dependently typed language supporting borrow
checking, designed for use as an intermediate representation for building
verifiable systems languages.
isotope
is composed of two languages: the “main” or “implementation” language,
and a “term” language. Expressions in the “main” language describe dependently
typed RVSDGs extended with lifetimes, which are given denotations in the
“term” language, which ignores low-level details such as lifetimes and
representation. In turn, the types of these expressions may depend only on
values in the “term” language, with programs, representations, and “main”
language types themselves values like any other. The “term” language itself is a
simplified implementation of the Calculus of Constructions, inspired by
Lean, extended with Zombie-like support for congruence-based normalization.
Re-exports
pub use error::Error; |
Modules
ast | Convert |
builder | Convert |
ctx | Contexts for creating, normalizing, and type-checking |
error | Error handling utilities |
prelude | Commonly used items |
primitive | Primitive |
program |
|
repr | Machine representations for |
term | Terms in |
typing | Datatypes for |
utils | Utilities |
Macros
for_annot_ref | Return the same expression for every variant of |
for_term | Return the same expression for every variant of |